\begin{tabbing}
$\forall$\=$X$:Type\{j\}, $x_{1}$:es\_realizer\{i:l\}, ${\it none}$:$X$, ${\it plus}$:(\=es\_realizer\{i:l\}$\rightarrow$es\_realizer\{i:l\}$\rightarrow$$X$$\rightarrow$$X$$\rightarrow$\+\+
\\[0ex]$X$),
\-\\[0ex]${\it init}$:(Id$\rightarrow$($T$:Type\{i\}$\rightarrow$Id$\rightarrow$($T$ + (rationals$\rightarrow$$T$))$\rightarrow$$X$)),
\\[0ex]${\it frame}$:(Id$\rightarrow$Type\{i\}$\rightarrow$Id$\rightarrow$(Knd List)$\rightarrow$$X$), ${\it sframe}$:(IdLnk$\rightarrow$Id$\rightarrow$(Knd List)$\rightarrow$$X$),
\\[0ex]${\it effect}$:(Id$\rightarrow$(\=${\it ds}$:fpf(Id; $x$.Type\{i\})$\rightarrow$Knd$\rightarrow$\+
\\[0ex](\=$T$:Type\{i\}$\rightarrow$$x$:Id$\rightarrow$(\=(decl{-}state(${\it ds}$)$\rightarrow$$T$$\rightarrow$decl{-}type\=\{i:l\}\+\+\+
\\[0ex](${\it ds}$; $x$)) + (decl{-}state(${\it ds}$)$\rightarrow$
\-\\[0ex]$T$$\rightarrow$rationals$\rightarrow$decl{-}type\=\{i:l\}\+
\\[0ex](${\it ds}$; $x$)))
\-\-\\[0ex]$\rightarrow$$X$))),
\-\-\\[0ex]${\it sends}$:(\=${\it ds}$:fpf(Id; $x$.Type\{i\})$\rightarrow$Knd$\rightarrow$\+
\\[0ex]($T$:Type\{i\}$\rightarrow$IdLnk$\rightarrow$(\=${\it dt}$:fpf(Id; $x$.Type\{i\})$\rightarrow$\+
\\[0ex](\=(${\it tg}$:Id\+
\\[0ex]$\times$ (decl{-}state(${\it ds}$)$\rightarrow$$T$$\rightarrow$(decl{-}type\=\{i:l\}\+
\\[0ex](${\it dt}$; ${\it tg}$) List))) List)
\-\-\\[0ex]$\rightarrow$$X$))),
\-\-\\[0ex]${\it pre}$:(Id$\rightarrow$(${\it ds}$:fpf(Id; $x$.Type\{i\})$\rightarrow$Id$\rightarrow$finite{-}prob{-}space$\rightarrow$(decl{-}state(${\it ds}$)$\rightarrow\mathbb{B}$)$\rightarrow$$X$)),
\\[0ex]${\it aframe}$:(Id$\rightarrow$Knd$\rightarrow$(Id List)$\rightarrow$$X$), ${\it bframe}$:(Id$\rightarrow$Knd$\rightarrow$(IdLnk List)$\rightarrow$$X$),
\\[0ex]${\it rframe}$:(Id$\rightarrow$Id$\rightarrow$(Knd List)$\rightarrow$$X$).
\-\\[0ex]es\_realizer\_ind(\=$x_{1}$;\+
\\[0ex]${\it none}$;
\\[0ex]${\it left}$,${\it right}$,${\it rec}_{1}$,${\it rec}_{2}$.${\it plus}$(${\it left}$,${\it right}$,${\it rec}_{1}$,${\it rec}_{2}$);
\\[0ex]${\it loc}$,$T$,$x$,$v$.${\it init}$(${\it loc}$,$T$,$x$,$v$);
\\[0ex]${\it loc}$,$T$,$x$,$L$.${\it frame}$(${\it loc}$,$T$,$x$,$L$);
\\[0ex]${\it lnk}$,${\it tag}$,$L$.${\it sframe}$(${\it lnk}$,${\it tag}$,$L$);
\\[0ex]${\it loc}$,${\it ds}$,${\it knd}$,$T$,$x$,$f$.${\it effect}$(${\it loc}$,${\it ds}$,${\it knd}$,$T$,$x$,$f$);
\\[0ex]${\it ds}$,${\it knd}$,$T$,$l$,${\it dt}$,$g$.${\it sends}$(${\it ds}$,${\it knd}$,$T$,$l$,${\it dt}$,$g$);
\\[0ex]${\it loc}$,${\it ds}$,$a$,$p$,$P$.${\it pre}$(${\it loc}$,${\it ds}$,$a$,$p$,$P$);
\\[0ex]${\it loc}$,$k$,$L$.${\it aframe}$(${\it loc}$,$k$,$L$);
\\[0ex]${\it loc}$,$k$,$L$.${\it bframe}$(${\it loc}$,$k$,$L$);
\\[0ex]${\it loc}$,$x$,$L$.${\it rframe}$(${\it loc}$,$x$,$L$))
\-\\[0ex]$\in$ $X$
\end{tabbing}